{-# LANGUAGE TypeFamilies, PolyKinds, UndecidableInstances, DataKinds #-}

module TypeBasics (module MaybeKind, Apply, IdT, ConstT,
                   True, False, ToBool, FromBool,
                   If, Not, Or, And, AndT, OrT,
                   Proxy(..),
                   Equal,
                   Codomain,
                   IsPrefixOf,
                   derive, encode
                  ) where

import Type.Spine
import Type.Ord (IsEQ)
import Type.Serialize
import Type.Ord.SpineSerialize (Compare)
import qualified Type.Booleans as BStar
import MaybeKind



type family Apply fn a

data IdT
data ConstT b

type instance Apply IdT a = a
type instance Apply (ConstT b) a = b



type True  = 'True
type False = 'False

type family ToBool (a :: *) :: Bool
type instance ToBool BStar.True = True
type instance ToBool BStar.False = False

type family FromBool (a :: Bool) :: *
type instance FromBool True = BStar.True
type instance FromBool False = BStar.False

type family If (b :: Bool) (x :: *) (y :: *) :: *
type instance If True  x y = x
type instance If False x y = y

type family Not (b :: Bool) :: Bool
type instance Not True = False
type instance Not False = True

type family Or (b1 :: Bool) (b2 :: Bool) :: Bool
type instance Or True  x = True
type instance Or False x = x

type family And (b1 :: Bool) (b2 :: Bool) :: Bool
type instance And True  x = x
type instance And False x = False



data AndT   ;   data AndT' a
data OrT    ;   data OrT' a

type instance Apply AndT a = AndT' a
type instance Apply OrT  a = OrT' a

type instance Apply (AndT' a) b = FromBool (And a b)
type instance Apply (OrT'  a) b = FromBool (Or a b)






type Equal a b = ToBool (IsEQ (Compare a b))



type family IsPrefixOf (pre :: *) (s :: *) :: Bool -- emulated primitive



data Proxy a = Proxy



type family Codomain (fn :: *) :: *
type instance Codomain (a -> b) = b





derive n = do
  d <- spineType n
  (d ++) `fmap` serializeTypeAsHash n
